Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
This is a subentry of (∞,1)-Grothendieck construction.
When (∞,1)-categories are modeled as quasi-categories, the (∞,1)-Grothendieck construction takes the form of a Quillen equivalence between a model structure on sSet-enriched presheaves and a slice model structure of simplicial sets which has been introduced under the name straightening and unstraightening in Lurie 2009, Sec. 3.2:
Concretely, in the notation recalled at relation between quasi-categories and simplicial categories:
For a simplicial set , simplicially enriched category , and sSet-enriched functor , there is a pair of adjoint functors
which (under an assumption on the parameter ) can be shown to be a Quillen equivalence between
the slice category of sSet equipped with the model structure for right fibrations (also called contravariant model structure in HTT)
the category of simplicial presheaves equipped with global projective model structure.
There is also a Quillen equivalence
between
the global projective model structure on functors with values in the model structure on marked simplicial sets.
In both cases,
is called the straightening functor
is called the unstraightening functor.
These names have been chosen due to the fact that objects in the left hand category are defined by existential assertions and choices where on the right side these properties become coherence laws being part of the structure.
The original result is due to:
Intuition of Lurie’s construction is discussed in:
Further discussion:
Danny Stevenson, Covariant Model Structures and Simplicial Localization, North-West. Eur. J. Math. 3 (2017) 141-202 [arXiv:1512.04815]
Gijs Heuts, Ieke Moerdijk, Left fibrations and homotopy colimits II [arXiv:1602.01274]
Alexander Campbell, A modular proof of the straightening theorem, talk at Macquarie University (2020) [pdf, pdf]
Fabian Hebestreit, Gijs Heuts, Jaco Ruit, A short proof of the straightening theorem (arXiv:2111.00069).
Discussion internal to any (∞,1)-topos:
Discussion of straightening and unstraightening entirely within the context of quasi-categories:
which (along the lines of the discussion of the universal left fibration from Cisinski 2019) allows to understand the universal coCartesian fibration as categorical semantics for the univalent type universe in directed homotopy type theory:
(see video 3 at 1:16:58 and slide 3.33).
Discussion of straightening and unstraightening for (∞,n)-categories:
Last revised on June 22, 2024 at 10:01:08. See the history of this page for a list of all contributions to it.